package mac5789.sat;

import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;

/**
 * Problema criado manualmente.
 * 
 * @author lundberg
 * 
 */
public class CraftedSatProblem implements SatProblem {

    private String format = "cnf";

    private int variables = 0;

    private List<Integer[]> clauses = new ArrayList<Integer[]>();

    /**
     * {@inheritDoc}
     */
    @Override
    public Iterator<Integer[]> getClauses() {
        return this.clauses.iterator();
    }

    @Override
    public String getFormat() {
        return this.format;
    }

    /**
     * {@inheritDoc}
     */
    public int getNClauses() {
        return this.clauses.size();
    }

    /**
     * {@inheritDoc}
     */
    public int getNVariables() {
        return this.variables;
    }

    /**
     * {@inheritDoc}
     */
    @Override
    public Iterator<Integer[]> iterator() {
        return this.getClauses();
    }

    /**
     * Adiciona uma cláusula do problema
     * 
     * @param clause
     *            clause
     * @return problem
     */
    public CraftedSatProblem add(Integer... clause) {
        for (Integer literal : clause) {
            this.variables = Math.max(this.variables, Math.abs(literal));
        }
        this.clauses.add(clause);
        return this;
    }

    /**
     * Adiciona uma cláusula do problema
     * 
     * @param clause
     *            clause
     * @return problem
     */
    public CraftedSatProblem add(List<Integer> clause) {
        return this.add(clause.toArray(new Integer[clause.size()]));
    }
}
